ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), m:.
ecl-act(ds;da;m;x)  (event-info(ds;da) List)Prop 

latex

Definitions	x:A. B(x), , t  T, Prop, ecl-act(ds;da;m;x), False, P  Q, x:A. B(x), P & Q, P  Q, x,y. t(x;y), x,y,z,w. t(x;y;z;w), AB, A, x,y,z. t(x;y;z), x. t(x), x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), x(s), S  T
Lemmas	ecl ind wf, event-info wf, false wf, decl-state wf, ma-valtype wf, bool wf, append wf, ecl-halt wf, le wf, nat plus wf, iseg wf, nat plus inc, nat wf, star-append wf, ifthenelse wf, eq int wf, ecl wf, fpf wf, Knd wf, Id wf